Nuprl Lemma : no_repeats-pairs-fpf
0,22
postcript
pdf
A
,
B
:Type,
eq1
:EqDecider(
A
),
eq2
:EqDecider(
B
),
L
:(
A
B
) List. no_repeats(
A
;fpf-domain(fpf(
L
)))
latex
Definitions
EqDecider(
T
)
,
no_repeats(
T
;
l
)
,
t
T
,
P
&
Q
,
x
:
A
.
B
(
x
)
Lemmas
deq
wf
,
pairs-fpf
property
origin
A, B:Type, eq1:EqDecider(A), eq2:EqDecider(B), L:(A
B) List. no_repeats(A;fpf-domain(fpf(L))) A, B:Type, eq1:EqDecider(A), eq2:EqDecider(B), L:(AB) List. no_repeats(A;fpf-domain(fpf(L))) 
Tx:A. B(x)